/**
 * 符号用于表示谓词、函数名或者常量
 */
class Sym {
    name: string;
    constructor(name: string) {
        this.name = name;
    }
    rename(nm: number) {
        return this;
    }
    //sym的rewrite永远返回自己
    rewrite(env: any) { return this; }
    toAnswerString() { return this.name }

    /**
     * unify是找到使两个术语相等的替换过程
     * @param that 
     * @param env 
     */
    unify(that: Sym|Var, env: any) {
        if (that instanceof Sym)
            //如果对方也是Sym，则只要名字相同就能统一
            assert(this.name == that.name)
        else {
            assert(that instanceof Var)
            // 如果对方是变量，则用变量的值进行unify
            if (env[that.name])
                this.unify(env[that.name], env)
            else
                addBinding(env, that.name, this.rewrite(env))
        }
    }
}

/**
 * 变量。可以与其他对象进行unify以获得具体的值
 */
class Var {
    name: string;
    constructor(name: string) {
        this.name = name;
    }

    rename(nm: number) { return new Var(this.name + nm) }

    /**
     * 根据替换映射重写对象
     * @param env 
     * @returns 
     */
    rewrite(env: any) { return env[this.name] ? env[this.name] : this }

    /**
     * 用于显示答案的字符串表示
     * @returns 
     */
    toAnswerString() { return this.name }

    unify(that:Sym|Var, env:any) {
        if (env[this.name]) //这时候变量已经有一个绑定的值了，所以用这个值与that进行unify
          env[this.name].unify(that, env)
        else
          addBinding(env, this.name, that.rewrite(env))
      }    
}

/**
 * 子句对象。
 * 由一个Sym和一组参数组成的逻辑语句。
 * 用于表示规则、事实或者查询
 * 由一个head和>=0个参数组成，描述了某种逻辑关系或者条件
 */
class Clause {
    sym: Sym;
    args: any;
    constructor(sym: Sym, args: any) { this.sym = sym; this.args = args }
    rename(nm: number) { return new Clause(this.sym, this.args.map(function (x:Var|Sym) { return x.rename(nm) })) }

    rewrite(env: any) { return new Clause(this.sym, this.args.map(function (x:Var|Sym) { return x.rewrite(env) })) }
    toAnswerString() {
        return this.sym.toAnswerString() + "(" + this.args.map(function (x:Var|Sym) { return x.toAnswerString() }).join(", ") + ")"
    }

    unify(that: Clause | Sym | Var, env: any) {
        if (that instanceof Clause) {
            //都是Clause的话，则符号和参数列表都要一致
            this.sym.unify(that.sym, env)
            assert(that.args.length == this.args.length)
            for (var idx = 0; idx < this.args.length; idx++)
                this.args[idx].unify(that.args[idx], env)
        }
        else
            //如果对方不是clause
            that.unify(this as any, env)
    }
}


// Array.prototype.rename  = function(n:number)   { return this.map(function(x) { return x.rename(n) }) }
// Array.prototype.rewrite = function(env:any) { return this.map(function(x) { return x.rewrite(env) }) }
// Array.prototype.toAnswerString = function() { return this.map(function(x) { return x.toAnswerString() }).join(", ") }

/**
 * 规则是由子句（Clause）组成
 */
class Rule {
    //规则的头
    head: Clause;
    //规则的目标，当规则的目标成立时，规则的头部也成立。 没有目标则是事实？
    clauses: Clause[];
    constructor(head: Clause, clauses: Clause[]) { this.head = head; this.clauses = clauses }
    rename(n: number) { 
        return new Rule(this.head.rename(n), this.clauses.map(x=>x.rename(n))) 
    }
}

function addBinding(env:any, name:string, value:Sym|Var) {
  var subst:any = {}
  subst[name] = value
  for (var n in env)
    if (env.hasOwnProperty(n))
      env[n] = env[n].rewrite(subst)
  env[name] = value
}

function assert(cond:boolean) { if (!cond) throw "unification failed" }


class State{
    query:Clause;  
    goals;
    /**
     * 查询和目标列表
     * @param query 
     * @param goals 
     */
    constructor(query:Clause, goals:Clause[]) { this.query = query; this.goals = goals }
}

function nextSolution(nameMangler:number, rules: Rule[], stateStack: State[]) {
    while (true) {
        // 堆栈为空了则结束
        if (stateStack.length == 0)
            return false

        // 取出最上面的状态
        var state = stateStack.pop(),
            query = state.query,
            goals = state.goals

        if (goals.length == 0){
            //return !window.confirm(query.toAnswerString())
            let answer = query.toAnswerString()
            console.log('answer:',answer)
            return answer;
        }
        var goal = goals.pop()

        // 逆序遍历规则列表
        for (var idx = rules.length - 1; idx >= 0; idx--) {
            var rule = rules[idx].rename(nameMangler), env:any;
            // 如果unify操作没有异常，则表示统一成功，可以更新状态
            try { rule.head.unify(goal, env = {}) } //创建一个当前env
            catch (e) { continue }
            // 新的查询和目标
            var newQuery = query.rewrite(env),
                newGoals = goals.map(x=>x.rewrite(env)), //goals.rewrite(env),
                newBody = rule.clauses.map(x=>x.rewrite(env))
            for (var idx2 = newBody.length - 1; idx2 >= 0; idx2--)
                newGoals.push(newBody[idx2])
            stateStack.push(new State(newQuery, newGoals))
        }
    }
}

function solve(query:Clause, rules:Rule[]) {
  var stateStack = [new State(query, [query])], n = 0
  while (nextSolution(n++, rules, stateStack)) {}
  console.log("no more solutions")
}

export class TinyProlog{
    test(){
        solve(
            //查询
            new Clause(new Sym("grandfather"), [new Sym("abe"), new Var("X")]),
        
            //规则
            [new Rule(new Clause(new Sym("grandfather"), [new Var("X"), new Var("Y")]),
                      [new Clause(new Sym("father"), [new Var("X"), new Var("Z")]),
                       new Clause(new Sym("father"), [new Var("Z"), new Var("Y")])]),
        
             new Rule(new Clause(new Sym("father"), [new Sym("abe"), new Sym("homer")]), []),
             new Rule(new Clause(new Sym("father"), [new Sym("homer"), new Sym("lisa")]), []),
             new Rule(new Clause(new Sym("father"), [new Sym("homer"), new Sym("bart")]), [])]
          )
        
    }
}

/*
A couple of examples:

solve(
  new Clause(new Sym("nat"), [new Var("X")]),
  [new Rule(new Clause(new Sym("nat"), [new Sym("z")]), []),
   new Rule(new Clause(new Sym("nat"), [new Clause(new Sym("s"), [new Var("X")])]),
            [new Clause(new Sym("nat"), [new Var("X")])])]
)

solve(
  new Clause(new Sym("grandfather"), [new Sym("abe"), new Var("X")]),
  [new Rule(new Clause(new Sym("grandfather"), [new Var("X"), new Var("Y")]),
            [new Clause(new Sym("father"), [new Var("X"), new Var("Z")]),
             new Clause(new Sym("father"), [new Var("Z"), new Var("Y")])]),
   new Rule(new Clause(new Sym("father"), [new Sym("abe"), new Sym("homer")]), []),
   new Rule(new Clause(new Sym("father"), [new Sym("homer"), new Sym("lisa")]), []),
   new Rule(new Clause(new Sym("father"), [new Sym("homer"), new Sym("bart")]), [])]
)

*/


  /*
    1. grandfather(X,Y):= father(X,Z) && father(Z,Y)
    2. father('abe','homer')
    3. father('homer','lisa')
    4. father('homer','bart')

    查询abe是谁的grandfather
    grandfather('abe',X) 

  */